/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.symm;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Random;
import java.util.Set;
import java.util.TreeMap;
import java.util.Vector;

import alloy.type.BasicType;
import alloy.util.Dbg;

//-------------------------------------------------
//class Symmetry
//-------------------------------------------------
/**
 * A symmetry of system: a permutation of each basic type.
 * Since the atoms of the basic types are defined to be indistinguishable,
 * any product of basic type permutations is a symmetry of the model.
 */
class Symmetry implements Comparable {

    /**
     * For each basic type, a permutation, expressed as int array of target indices.
     * If basic type not present, its permutation is the identity.
     * {@link Map} from {@link BasicType} to an int[].
     */
    private Map /* BasicType->int[] */ _domPerm = new TreeMap();

    /** Cached string value */
    private String _cachedStringValue;

    public void makeImmutable() { _cachedStringValue = toString(); }
    public boolean isImmutable() { return _cachedStringValue != null; }

    /** Test whether this symmetry permutes a basic type, or leaves it in place */
    boolean permutes(BasicType d_) { return _domPerm.containsKey(d_); }

    /** Return the target of a basic type's atom under this permutation */
    int getTargetAtom(BasicType d_, int atom_) {
        int[] dperm = (int[])_domPerm.get(d_);
        return dperm==null ? atom_ : dperm[atom_];
    }

    /** Return the {@link Set} of {@link BasicType}s permuted by this symmetry */
    Set /* of BasicType */ getPermutedTypes() { return _domPerm.keySet(); }

    /**
     * Test whether this symmetry stabilizes a given range of basic
     * type atoms, i.e. whether it permutes these atoms among themselves.
     */
    boolean stabilizes(BasicType basicType_, int fromAtom_, int toAtom_) {
        int[] map = (int[])_domPerm.get(basicType_);
        if (map != null) {
            for (int atom=fromAtom_; atom<toAtom_; atom++) {
            int targetAtom = map[atom];
            if (targetAtom < fromAtom_  ||
                targetAtom >= toAtom_)
                return false;
            }
        }
        return true;
    }

    /**
     * Set the target of a basic type's atom under this permutation.  This may
     * temporarily make the permutation invalid; this method can be
     * used for construction, but validity of the symmetry should
     * be verified by calling {@link #isValidPermutation} before use.
     */
    void setTargetAtom(BasicType d_, int atom_, int target_) {
        Dbg.chk(!isImmutable());
        if (!permutes(d_)) _domPerm.put(d_, new int[d_.getScope()]);
        Dbg.chk(permutes(d_));
        int[] dperm = (int[])_domPerm.get(d_);
        dperm[atom_] = target_;
        }

        /** Specify how the symmetry permutes a particular basic type. */
        void setBasicTypePerm(BasicType btype_, int[] targets_) {
        Dbg.chk(!isImmutable());
        _domPerm.put(btype_, targets_);
    }

    /** Construct an identity symmetry*/
    Symmetry() { }

    /** Construct a transposition of two elements */
    static Symmetry createTransposition(BasicType d_, int atom1_, int atom2_) {
        Symmetry s = new Symmetry();
        int[] dperm = new int[d_.getScope()];
        for (int i=0; i<dperm.length; i++)
            dperm[i] = i==atom1_ ? atom2_ : (i==atom2_ ? atom1_ : i);
        s._domPerm.put(d_, dperm);
        s.makeImmutable();
        return s;
    }

    /** For a {@link BasicType}, construct single-cycle symmetries which rotate
    the atoms, e.g. for (123), we return the list [(312), (231)].
    @return {@link List} of {@link Symmetry}s */
    static List createRotSymmetries(BasicType d_) {
        List rotSymms = new ArrayList();
        for (int shiftAmt = 1; shiftAmt < d_.getScope(); shiftAmt++) {
            Symmetry s = new Symmetry();
            int[] dperm = new int[d_.getScope()];
            for (int i=0; i<d_.getScope(); i++)
            dperm[i] = (i + shiftAmt) % d_.getScope();
            Dbg.chk(s.isValidPermutation());
            s.makeImmutable();
            rotSymms.add(s);

        }

        return rotSymms;
    }

    /** Compute the number of cycles in the symmetry */
    int computeNumCycles() {
        int numCycles = 0;
        int[] dperm = (int[])((Map.Entry)_domPerm.entrySet().iterator().next()).getValue();
        boolean[] seen = new boolean[dperm.length];
        for (int i=0; i<dperm.length; i++) {
            if (seen[i]) continue;
            int j = i;
            do {
            seen[j] = true;
            j = dperm[j];
            } while (j != i);
            numCycles++;
        }
        return numCycles;
    }

    /** Create a random symmetry */
    static Symmetry createRandomSymmetry(Set domains_, Random rand_) {
        Symmetry s = new Symmetry();
        // System.out.println("Creating new symmetry");

        for (Iterator domIter = domains_.iterator(); domIter.hasNext();) {
            BasicType dom = (BasicType)domIter.next();
            // System.out.println("On domain: " + dom);
            int[] perm = new int[dom.getScope()];
            boolean[] taken = new boolean[dom.getScope()];
            for (int i=0; i<taken.length; i++)
            taken[i] = false;
            for (int i=0; i<perm.length; i++) {
            // determine the target of atom <i> of domain <dom>
            // System.out.println("targeting atom " + i);
            int n = rand_.nextInt(perm.length - i);
            // System.out.println("to " + n + "th unocc. slot");
            // map atom <i> to <n>'th unoccupied slot
            int target;
            for (target=0; target<perm.length; target++) {
                // System.out.println("Looking at target " + target);
                // System.out.println("taken=" + taken[target] + " n=" + n);
                if (!taken[target]) {
                if (n>0)
                    n--;
                else {
                    perm[i] = target;
                    taken[target] = true;
                    break;
                }
                }
            }
            }
            s._domPerm.put(dom, perm);
        }
        if (!s.isValidPermutation()) throw new Error("invalid random permutation");
        // System.out.println("Created symmetry: " + s);
        s.makeImmutable();
        return s;
    }

    /** Compose: return a symmetry that applies first theta_, then this */
//     Symmetry compose(Symmetry theta_) {
//  Symmetry r = new Symmetry();
//  // for each domain permuted by theta_, apply theta_'s permutation then ours
//  for (Enumeration d = theta_._domPerm.keys(); d.hasMoreElements();) {
//      BasicType domain = (BasicType)d.nextElement();
//      for (int atom=0; atom<domain.get_scope(); atom++)
//      r.setTargetAtom(domain, atom,
//              getTargetAtom(domain,
//                        theta_.getTargetAtom(domain, atom)));
//  }
//  // for each domain not permuted by theta_ but permuted by this,
//  // apply the permutation done by this
//  for (Enumeration d = _domPerm.keys(); d.hasMoreElements();) {
//      BasicType domain = (BasicType)d.nextElement();
//      if (!theta_.permutes(domain))
//      for (int atom=0; atom < domain_.get_scope(); atom++)
//          r.setTargetAtom(domain, atom, getTargetAtom(domain, atom));
//  }
//  return r;
//     }

    /** Test whether this Symmetry object represents a valid permutation */
    boolean isValidPermutation() {
        Vector doms = new Vector();
        for (Iterator d = _domPerm.keySet().iterator(); d.hasNext();) {
            BasicType dom = (BasicType)d.next();
            if (doms.contains(dom)) return false;
            doms.addElement(dom);
            int[] perm = (int[])_domPerm.get(dom);
            if (perm.length != dom.getScope()) return false;
            boolean[] used = new boolean[perm.length];
            for (int i=0; i<used.length; i++) used[i] = false;
            for (int i=0; i<perm.length; i++) {
            if (used[perm[i]]) return false;
            used[perm[i]] = true;
            }
            for (int i=0; i<used.length; i++)
            if (!used[i]) return false;
        }
        return true;
    }

    public String toString() {
        if (_cachedStringValue != null) return _cachedStringValue;
        String r = "{";
        for (Iterator d = _domPerm.keySet().iterator(); d.hasNext();) {
            BasicType dom = (BasicType)d.next();
            int[] dperm = (int[])_domPerm.get(dom);
            r += dom.toString() + "[";
            for (int i=0; i<dperm.length; i++)
            r += dperm[i] + (i==dperm.length-1 ? "" : ",");
            r += "]";
        }
        return r + "}";
    }

    public boolean equals(Object obj_) {
        return obj_!=null && obj_.getClass().equals(this.getClass()) &&
            obj_.toString().equals(this.toString());
    }

    public int hashCode() { return toString().hashCode(); }

    public int compareTo(Object obj_) {
        Symmetry thatSymm = (Symmetry)obj_;
        return toString().compareTo(thatSymm.toString());
    }
}  // class Symmetry


